Nuprl Definition : f-event 11,40

f-event{$x:ut2}
f-event(es; L; e)
== (loc(e)  L) c ((es-after(es; mkid{$x:ut2}; e) = es-when(es; mkid{$x:ut2}; e))) 
latex



clarification:

f-event{$x:ut2}
f-event(es; L; e)
== (es-loc(es; e)  L  Id)
== c ((es-after(es; mkid{$x:ut2}; e) = es-when(es; mkid{$x:ut2}; e)  Id)) 
latex


DefinitionsA c B, (x  l), loc(e), A, s = t, Id, es-after(es; x; e), es-when(es; x; e), mkid{$x:ut2}
FDL editor aliasesf-event

origin